Operational semantics.md (7967B)
1 +++ 2 title = 'Operational semantics' 3 +++ 4 # Operational semantics 5 ## Creating a small imperative language: WHILE 6 WHILE has the grammar: 7 8 ``` 9 S ::= skip -- no-op 10 | x := a -- assignment 11 | S; S -- sequence of statements 12 | if b then S else S -- conditional statement 13 | while b do S -- while loop 14 ``` 15 16 It can be represented in Lean with an inductive type: 17 18 ```lean 19 inductive stmt : Type 20 | skip : stmt 21 | assign : string → (state → Ν) → stmt 22 | seq : stmt → stmt → stmt 23 | ite : (state → Prop) → stmt → stmt → stmt 24 | while : (state → Prop) → stmt → stmt 25 26 infixr ` ;; ` : 90 := stmt.seq 27 ``` 28 29 The state is basically the environment, resolving a string to a value. 30 Then we can write a program: 31 32 ```lean 33 def prog1 : stmt := 34 stmt.while (λs, s "y" > 0) 35 (stmt.skip ;; stmt.assign "x" (λs, s "a" + s "b")) 36 ``` 37 38 Deep embedding: abstract syntax tree specified in proof assistant, along with semantics 39 Shallow embedding: reuses mechanisms from logic (λ-terms, functions, predicate types) 40 41 ## Big-step (natural) semantics 42 Judgments have the form `(S, s) ⇒ t`: starting in state `s`, executing `S` terminates in state `t`. 43 44 Derivation rules: 45 46 ``` 47 ——————————————— Skip 48 (skip, s) ⟹ s 49 50 51 ——————————————————————————— Asn 52 (x := a, s) ⟹ s[x ↦ s(a)] 53 54 55 (S, s) ⟹ t (T, t) ⟹ u 56 ——————————————————————————— Seq 57 (S; T, s) ⟹ u 58 59 60 (S, s) ⟹ t 61 ————————————————————————————— If-True if s(b) is true 62 (if b then S else T, s) ⟹ t 63 64 65 (T, s) ⟹ t 66 ————————————————————————————— If-False if s(b) is false 67 (if b then S else T, s) ⟹ t 68 69 70 (S, s) ⟹ t (while b do S, t) ⟹ u 71 —————————————————————————————————————— While-True if s(b) is true 72 (while b do S, s) ⟹ u 73 74 75 ————————————————————————— While-False if s(b) is false 76 (while b do S, s) ⟹ s 77 ``` 78 79 Specifying the rules in Lean: 80 81 ```lean 82 inductive big_step : stmt × state → state → Prop 83 | skip {s} 84 : big_step (stmt.skip, s) s 85 | assign {x a s} 86 : big_step (stmt.assign x a, s) (s{x ↦ a s}) 87 | seq {S T s t u} 88 (hS : big_step (S, s) t) 89 (hT : big_step (T, t) u) 90 : big_step (S ;; T, s) u 91 | ite_true {b : state → Prop} {S T s t} 92 (hcond : b s) 93 (hbody : big_step (S, s) t) 94 : big_step (stmt.ite b S T, s) t 95 | ite_false {b : state → Prop} {S T s t} 96 (hcond : ¬ b s) 97 (hbody : big_step (T, s) t) 98 : big_step (stmt.ite b S T, s) t 99 | while_true {b : state → Prop} {S s t u} 100 (hcond : b s) 101 (hbody : big_step (S, s) t) 102 (hrest : big_step (stmt.while b S, t) u) 103 : big_step (stmt.while b S, s) u 104 | while_false {b : state → Prop} {S s} 105 (hcond : ¬ b s) 106 : big_step (stmt.while b S, s) s 107 108 infix ` ⟹ ` : 110 := big_step 109 ``` 110 111 ## Properties of big-step semantics 112 We can: 113 - prove properties of programming language, e.g. equivalence between programs and determinism 114 - reason about concrete programs, proving theorems relating to state transitions 115 116 ```lean 117 lemma big_step_deterministic {S s l r} (hl : (S, ⟹ l) (hr : (S, s) ⟹ r) : 118 l = r 119 begin 120 induction' hl, 121 case skip { cases' hr, refl }, 122 case assign { cases' hr, refl } 123 case seq : S T s t l hS hT ihS ihT { 124 cases' hr with _ _ _ _ _ _ _ t' _ hS' hT', 125 cases' ihS hS', 126 cases' ihT hT', 127 refl }, 128 case ite_true : b S T s t hb hS ih { 129 cases' hr, 130 { apply ih hr }, 131 { cc } }, 132 ... 133 end 134 ``` 135 136 For termination, it's unprovable, but you can generate a counterexample and prove that it doesn't terminate: 137 138 ```lean 139 lemma big_step_doesnt_terminate {S s t} : 140 ¬ (stmt.while (λ_, true) S, s) ⟹ t := 141 begin 142 intro hw, 143 induction' hw, 144 case while_true {assumption}, 145 case while_false {cc} 146 end 147 ``` 148 149 ## Small-step semantics 150 Big-step semantics doesn't let us reason about intermediate states, or express nontermination or interleaving. 151 You can do this with small-step semantics (structural operational semantics). 152 153 A judgment has form `(S, s) ⇒ (T, t)`: starting in state `s`, executing one step of `S` leaves us in state `t`, with program `T` remaining to run. 154 A pair `(S, s)` is a "configuration". It's "final" if there's no transition from it. 155 156 Derivation rules: 157 158 ``` 159 ————————————————————————————————— Asn 160 (x := a, s) ⇒ (skip, s[x ↦ s(a)]) 161 162 163 (S, s) ⇒ (S', s') 164 ———-————————————————————— Seq-Step 165 (S ; T, s) ⇒ (S' ; T, s') 166 167 168 —————————————————————— Seq-Skip 169 (skip ; S, s) ⇒ (S, s) 170 171 172 ———————————————————————————————— If-True if s(b) is true 173 (if b then S else T, s) ⇒ (S, s) 174 175 176 ———————————————————————————————— If-False if s(b) is false 177 (if b then S else T, s) ⇒ (T, s) 178 179 180 ——————————————————————————————————————————————————————————————— While 181 (while b do S, s) ⇒ (if b then (S ; while b do S) else skip, s) 182 ``` 183 184 The Lean specification: 185 186 ```lean 187 inductive small_step : stmt × state → stmt × state → Prop 188 | assign {x a s} 189 : small_step (stmt.assign x a, s) (stmt.skip, s{x ↦ a s}) 190 | seq_step {S S' T s s'} 191 (hS : small_step (S, s) (S', s')) 192 : small_step (S ;; T, s) (S' ;; T, s') 193 | seq_skip {T s} 194 : small_step (stmt.skip ;; T, s) (T, s) 195 | ite_true {b : state → Prop} {S T s} 196 (hcond : bs) 197 : small_step (stmt.ite b S T, s) (S, s) 198 | ite_false {b : state → Prop} {S T s} 199 (hcond : ¬ b s) 200 : small_step (stmt.ite b S T, s) (T, s) 201 | while {b : state → Prop} {S s} 202 : small_step (stmt.while b S, s) (stmt.ite b (S ;; stmt.while b S) stmt.skip, s) 203 204 infixr ` ⇒ ` := small_step 205 infixr ` ⇒* ` : 100 := star small_step 206 ``` 207 208 We can define big-step semantics based on small-step: `(S, s) ⟹ t` iff `(S, s) ⇒* (skip, t)` (i.e. we can get to a `skip` in one or more small steps). 209 The `*` is the reflexive transitive closure. 210 211 ## Properties of small-step semantics 212 E.g. to show that a configuration is final only if the statement is a `skip`. 213 214 ```lean 215 lemma small_step_final (S s) : 216 (¬∃ T t, (S, s) ⇒ (T, t)) ↔ S = stmt.skip := 217 begin 218 induction' S, 219 case skip {simp, intros T t hstep, cases' hstep }, 220 case assign : x a { 221 simp, 222 apply exists.intro stmt.skip, 223 apply exists.intro s{x ↦ a s}), 224 exact small_step.assign }, 225 case seq : S T ihS ihT { 226 simp, 227 cases' classical.em (S = stmt.skip), 228 case inl { 229 rw h, 230 apply exists.intro T, 231 apply exists.intro s, 232 exact small_step.seq_skip }, 233 case inr { 234 simp [h, auto.not_foorall_eq, auto.not_not_eq] at ihs, 235 cases' ihS s with S' hS', 236 cases' hS' with s' hs', 237 apply exists.intro (S' ;; T), 238 apply exists.intro s', 239 exact small_step.seq_step hs' } }, 240 case ite : b S T ihS ihT { 241 simp, 242 cases' classical.em (b s), 243 case inl { 244 apply exists.intro S, 245 apply exists.intro s, 246 exact small_step.ite_true h }, 247 case inr { 248 apply exists.inro T, 249 apply exists.intro s, 250 exact small_step.ite_false h } }, 251 case while : b S ih { 252 simp, 253 apply exists.intro (stmt.ite b (S ;; stmt.while b S) stmt.skip), 254 apply exists.intro s, 255 exact small_step.while } 256 end 257 ``` 258